Nuprl Lemma : Rnone-icompat
11,40
postcript
pdf
A
:Realizer. R-icompat(Rnone();
A
)
latex
Definitions
tt
,
ff
,
True
,
Rnone?(
x1
)
,
Rplus-right(
x1
)
,
Rplus-left(
x1
)
,
P
&
Q
,
Rplus?(
x1
)
,
if
b
then
t
else
f
fi
,
Y
,
t
T
,
x
.
t
(
x
)
,
P
Q
,
,
R-icompat(
A
;
B
)
,
x
:
A
.
B
(
x
)
,
{
T
}
,
x
(
s
)
Lemmas
finite-prob-space
wf
,
bool
wf
,
fpf
wf
,
decl-type
wf
,
decl-state
wf
,
IdLnk
wf
,
Knd
wf
,
Id
wf
,
rationals
wf
,
es
realizer
wf
,
Rnone
wf
,
R-icompat
wf
,
es
realizer-induction
origin
A:Realizer. R-icompat(Rnone();A) A:Realizer. R-icompat(Rnone();A) 
T
x. t(x)
Q
x:A. B(x)